COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	Addenda to be integrated.
C00009 00004	.skip 1
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.AT "qt" ⊂"%At%*"⊃
.AT "qw" ⊂"%Aw%*"⊃
.AT "qi" ⊂"%5 -1%*"⊃
.AT "qm" ⊂"%Am%*"⊃
.cb EXOTIC AND EVEN PATHOLOGICAL CONTINUOUS FUNCTIONALS


	The fixed point theory of recursive functions is based on
continuous functionals such as

!!a1:	%2λf λx.(qif p x qthen g x qelse f h x)%1.

	The theory tells us that each continuous monotonic functional
has a fixed point, and we study the fixed points of those functionals
involved in recursive definitions.  However, these are not all the
continuous functions there are, and it may be interesting to study
some other examples.  Consider functionals of the form

!!a2:	%2qt[f](x) = qif p x qthen g x qelse m fqi h x%1;

that's right, we mean the inverse of the function %2f%1.  In order
to make the functional well defined and continuous, we make the
following stipulations:  First, the variable ⊗x ranges over non-negative
integers and ⊗f is a partial function from integers to integers.
Second, we define %2fqi%1 by

!!a3:	%2fqi(y) = qm x.(f(x) = y)%1,

where

!!a6:	%2qm x.p(x) ← least(0,p)%1,

and %2least(y,p)%1 is recursively defined by

!!a7:	%2least(y,p) ← qif p(y) qthen y qelse least(y+1,p)%1.

Note that the recursive definition insures that %2fqi%1 is continuous
in ⊗f, and that qmx.%2p(x)%1 is undefined if there is a value of
⊗x for which ⊗p(x) is undefined lower than a value for which ⊗p(x) 
is true.  Without this property, %2least(x,p)%1 wouldn't be monotonic
in %2p%1, and there mightn't be a least fixed point.

	Consider specializing ({eq a2}) to

!!a4:	%2qt1[f](x) = qif x = 0 qthen 0 qelse 2 + fqi(x - 1)%1.

The fixed point ⊗f1 of qt1 may be computed by iterating qt1 on %AW%1,
getting

!!a5:	%2f1 x = qif x = 0 qthen 0 qelse qif x = 1 qthen 2 qelse qif
x = 3 qthen 3 qelse qw%1,

which seems exotic if not pathological.

	Wolf Polak points out that while qt1 is exotic, its fixed point
is an ordinary recursive function, since the recursive computation
of %2fqi%1 can be spelled out.  Thus

!!a8:	%2f1 x ← qif x = 0 qthen 0 qelse 2 + f2(0,x-1)%1,

where

!!a9:	%2f2(y,x) ← qif f1(x) = y qthen x qelse f2(y+1,x)%1.

	Here is another weird functional:

!!a10:	%2qt2[f](x) = qif p x qthen g x qelse qif
f h1 x = qw ∧ f h2 x = qw qthen qw qelse f h3 x%1,

where ⊗p, ⊗g, ⊗h1, ⊗h2 and ⊗h3 are all assumed total.  (Equality here is
taken in the strong sense).
Computing it involves a parallel computation of %2f h1 x%1 and %2f h2 x%1;
if either succeeds, the other can be stopped.  It is easily seen that the
functional is continuous and hence has a fixed point - call it ⊗f2. 
If we can use Lisp functions, we can write an ordinary recursive
definition of ⊗f2, namely

!!a11:	%2f2 x ← qif p x qthen g x qelse (λy. f2 h3 x)(f2'(list(x),qNIL))%1,

with

!!a12:	%2f2'(u,v) ← qif qn u qthen (qn v ∨ f2(v,qnil))
qelse p h1 qa u ∨ p h2 qa u ∨ f2'(qd u, h1 qa u . (h2 qa u . v))%1.

If we are not allowed to use Lisp functions, then ⊗f2 may be one of
Hewitt's and Paterson's (197x) examples of functions that can be written
with parallel programs but not with recursive programs.
Addenda to be integrated.


	1. Additional continuous qt[f](x) include

a. f(x) ≠ qw for at least one x

b. f(x)+x ε A for at least 20 odd values of x

c. R1(x,f h1 x) ∧ R2(x,f f h2 x) for at least 20 x.

	2. Th 1. monotone ⊃ continuous for simple qt

Th2. qt[f](x) depends on only a finite number of values of f.

Th3. ordinary qt depend on a bounded number of values (uniformly continuous?)

Th4. ordinary qt are sequential.

The subclass of almost sequential.

The tree forms of continuous functionals.

The predicates play a special role an in fact the space whose elements
are just T and qw plays a special role.

Consider

	%2qt[f](x) = qif p1 x qthen g x qelse qif ∃z.(f h1 z ≠ qw) qthen
f h2 z qelse qw%1.

It is continuous.  It can't be computed for general ⊗f except by
parallel evaluator, but its fixed point can apparently be sequentially
computed provided the domain of ⊗x can be effectively enumerated.
You may be interested in EXOTIC[W77,JMC].  I would welcome your comments.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
EXOTIC[W77,JMC]
PUBbed at {time} on {date}.%1